Extraction hooks to support custom extraction by extensions #3058

nikswamy · 2023-09-27T23:35:01Z

This PR adds features in support of custom F* -> ML extraction by extension.

RT.dsl_tac_t, the type of the typed extension callback is changed as below, allowing an extension to store whatever metadata it wants, encoding as a "blob" (typically, a Tm_lazy { blob; lkind=Lazy_extension s}, for some choice of s).

(**
 * The type of the top-level tactic that would splice-in the definitions
 * It returns either:
 *   - Some tm, blob, typ, with a proof that `typing g tm typ`
 *   - None, blob, typ), with a proof that `exists tm. typing g tm typ`
 * The blob itself is optional and can store some additional metadata that
 * constructed by the tactic. If present, it will be stored in the 
 * sigmeta_extension_data field of the enclosing sigelt.
 *
 * The blob can be used later, e.g., during extraction, and passed back to the
 * extension to perform additional processing.
 *)
let blob = string & R.term
let dsl_tac_result_base_t = option R.term & option blob & R.typ
let well_typed g (e:dsl_tac_result_base_t) =
  let tm_opt, _, typ = e in
  match tm_opt with
  | None -> exists (tm:R.term). typing g tm (T.E_Total, typ)
  | Some tm -> typing g tm (T.E_Total, typ)

let dsl_tac_result_t g = e:dsl_tac_result_base_t { well_typed g e }

type dsl_tac_t = g:fstar_top_env -> T.Tac (dsl_tac_result_t g)

The returned blob from the extension is stored in a new field sigmeta_extension_data associating the extension name with the blob that it returned.
FStar.Extaction.ML.Modul exposes an extension hook:

type extension_extractor = 
   uenv -> FStar.Compiler.Dyn.dyn -> either (mlexpr * e_tag * mlty) string

val register_extension_extractor
         (extension_name:string)
         (extractor:extension_extractor)
  : unit

When extracting a top-level let binding, if the Sig_letbinding contains a sigmeta_extension_data, we see if we can find an extension_extractor registered for that extension data and if so, call it with the blob stored in the extension data.

Finally, to support the extraction of abstract types that model computations as primitive effects, there's a new attribute extract_as_impure_effect in pervasives, which is interpreted in FStar.Extraction.ML.Term when extracting types.

+(** A qualifier on a type definition which when used in co-domain position
+    on an arrow type will be extracted as if it were an impure effect type.
+
+    e.g., if you have
+
+    [@@extract_as_impure_effect]
+    val stt (a:Type) (pre:_) (post:_) : Type
+
+    then arrows of the form `a -> stt b p q` will be extracted
+    similarly to `a -> Dv b`.
+ *)
+val extract_as_impure_effect : unit

These features are used currently by steel/pulse to extract Pulse terms to F*'s ML AST, from where the rest of the extraction pipeline picks up to emit programs as either OCaml, or to C via krml (also relying there on pre-existing hooks to customize krml extraction)

…a mutable debug flag

…of coercions & polymorphism

…es like `Pulse.stt a p q` as if it were `Dv a`

…rivation, with corresponding proofs of typing

…t look at the top-most extension blob

nikswamy · 2023-09-28T00:28:38Z

src/extraction/FStar.Extraction.ML.Syntax.fst

+  | MLTY_Top -> "MLTY_Top"
+  | MLTY_Erased -> "MLTY_Erased"
+
+let rec mlexpr_to_string (e:mlexpr) =


This are just some printers, useful for debugging extraction

nikswamy · 2023-09-28T00:29:09Z

src/extraction/FStar.Extraction.ML.Term.fst

@@ -153,50 +154,57 @@ let effect_as_etag =
             where PC.result_type is an arity

 *)
-let rec is_arity env t =
+let rec is_arity_aux tcenv t =


Just a slight refactoring, since this function only needs tcenv

nikswamy · 2023-09-28T00:30:24Z

src/extraction/FStar.Extraction.ML.Term.fst

@@ -227,34 +235,52 @@ let rec is_type_aux env t =
      let t= U.ctx_uvar_typ u in
      is_arity env (SS.subst' s t)

-    | Tm_bvar ({sort=t})
-    | Tm_name ({sort=t}) ->
+    | Tm_bvar ({sort=t}) ->


This is a fix to prevent the compiler from relying on the bv.sort field in Tm_name.

Instead, we now look it up in the environment and are careful to push binders in the environment they are traversed

nikswamy · 2023-09-28T00:34:23Z

src/extraction/FStar.Extraction.ML.Term.fst

+        else (
+            if has_extract_as_impure_effect g fv
+            then let (a, _)::_ = args in
+                 translate_term_to_mlty g a


Just extract the first argument (the result type) in case fv has the "extract_as_impure_effect" attribute

nikswamy · 2023-09-28T00:35:01Z

src/extraction/FStar.Extraction.ML.Term.fst

+            let etag = effect_as_etag env (U.comp_effect_name c) in
+            let etag =
+              if etag = E_IMPURE then etag
+              else if head_of_type_is_extract_as_impure_effect env codom


Interpret fv's with extract_as_impure_effect as E_IMPURE

aseemr · 2023-09-28T04:04:18Z

src/syntax/FStar.Syntax.Syntax.fsti

@@ -620,6 +621,7 @@ type sig_metadata = {
    sigmeta_fact_db_ids:list string;
    sigmeta_admit:bool; //An internal flag to record that a sigelt's SMT proof should be admitted
                        //Used in DM4Free
+    sigmeta_extension_data: list (string & dyn) //each extension can register some data with a sig


In the extraction case, this would be a singleton list, right? Is there any other usage where this would be non-singleton?

So far, yes, this is singleton when used in extraction. But, I could imagine that different phases could stash different information in here, e.g, some extension data is added after tosyntax, some after typechecking, etc. Also, could one conceivably have multiple extensions process a single sigelt ... maybe?

aseemr · 2023-09-28T04:11:35Z

ulib/FStar.Ghost.fsti

@@ -45,6 +45,7 @@ module FStar.Ghost

 (** [erased t] is the computationally irrelevant counterpart of [t] *)
 [@@ erasable]
+new


Can you please comment on this change, just curious what was the trigger.

Not sure why this is still in this PR. I already pushed it separately to master:
08d80b8

the issue is that let test (x:erased int) (y:int) = x == y would succeed phase 1 and fail in phase 2. Marking erased as new (which it is) ensures that it also fails phase 1.

aseemr · 2023-09-28T04:14:26Z

ulib/FStar.Pervasives.fsti

+    then arrows of the form `a -> stt b p q` will be extracted 
+    similarly to `a -> Dv b`.
+ *)
+val extract_as_impure_effect : unit


I wonder if we should check this attribute, e.g., when typechecking a let definition, if it has the attribute, then allow only arrows whose codomain is impure effect?

Claiming that something is PURE is risky and would require checking. But, claiming that it is IMPURE is conservative, no?

aseemr · 2023-09-28T04:23:54Z

Thanks Nik, I have minor comments, we can discuss on the PR, but merging it since it is all green.

nikswamy added 11 commits September 19, 2023 21:11

hooks for a custom extraction pipeline for extensions

16145b9

print aqual attributes if ugly and print_implicits is on

55a0e3c

make eq_dbg use its dbg argument, rather than repeatedly reading the …

40c052d

…a mutable debug flag

mark erased as a new type, to get better type errors in the presence …

8efe706

…of coercions & polymorphism

Merge remote-tracking branch 'origin/master' into _nik_extraction

a0fa839

expose an normalize_for_extraction in FStar.Extraction.ML.Syntax

6ffe84a

a new attribute "extract_as_impure_effect", to support extracting typ…

505af3e

…es like `Pulse.stt a p q` as if it were `Dv a`

changing the type of RT.dsl_tac_t to return a blob and an optional de…

19a18ee

…rivation, with corresponding proofs of typing

undo a few spurious changes

1f8aba8

make blobs returned by dsl_tac_t optional

6bad8bc

refactor extraction of extension let bindings so that it does not jus…

6b9c065

…t look at the top-most extension blob

nikswamy commented Sep 28, 2023

View reviewed changes

nikswamy added 2 commits September 27, 2023 17:39

remove an unreachable case, since applications are explicitly flattened

7a58dad

snap

68b8464

aseemr reviewed Sep 28, 2023

View reviewed changes

aseemr merged commit d94c006 into master Sep 28, 2023
3 checks passed

aseemr deleted the nik_extraction branch September 28, 2023 04:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Extraction hooks to support custom extraction by extensions #3058

Extraction hooks to support custom extraction by extensions #3058

nikswamy commented Sep 27, 2023 •

edited

Loading

nikswamy Sep 28, 2023

nikswamy Sep 28, 2023

nikswamy Sep 28, 2023

nikswamy Sep 28, 2023

nikswamy Sep 28, 2023

aseemr Sep 28, 2023

nikswamy Sep 28, 2023

aseemr Sep 28, 2023

nikswamy Sep 28, 2023

nikswamy Sep 28, 2023

aseemr Sep 28, 2023

nikswamy Sep 28, 2023

aseemr commented Sep 28, 2023

Extraction hooks to support custom extraction by extensions #3058

Extraction hooks to support custom extraction by extensions #3058

Conversation

nikswamy commented Sep 27, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aseemr commented Sep 28, 2023

nikswamy commented Sep 27, 2023 •

edited

Loading